PROVING COMPILERS CORRECT

	The  abstract  study of  computer  programs  as  mathematical
objects  and the technology  of programming meet  when we  try to use
computers to verify that computer programs meet their specifications.
When the program to be proved correct  is a compiler, we have also to
formalize  the   syntax  and  semantics  of  the  source  and  target
languages.  A simple example will be fully treated.